T:Type, l:IdLnk, ds1, ds2:x:Id fp
Type, P:(State(ds1)
Prop), Q:(State(ds2)Prop),
f:(State(ds1)T).
Normal(T)
Normal(ds1)
Normal(ds2)
destination(l) = source(l) 
Id
(s:State(ds1). Dec(
k:. P(s,k)))
(s:State(ds2). Dec(k:. Q(s,k)))
(s:State(ds1), k:. Dec(P(s,k)))
(s:State(ds2), k:. Dec(Q(s,k)))
es.@source(l) state ds1 & (e:E. kind(e) = rcv(l,"tg") Knd valtype(e) 
T)
es.& @destination(l) state ds2
es.& (e:E. kind(e) = rcv(lnk-inv(l),"tg") Knd valtype(e) 
)
es. (k:. @source(l) stable s.P(s,k) )
es. (k:. @destination(l) stable s.Q(s,k) )
es. (k:.
es. (e@source(l).
es. (P(state after e,k)
es. ( e'@destination(l).Q((state when e'),k) 
(n:. Q(state after e',n)))
es. (e:E. kind(e) = rcv(lnk-inv(l),"tg") Knd (k:. k<val(e) P(state after e,k)))
es. (k:, e:E.
es. (kind(e) = rcv(l,"tg") Knd
es. ( val(e) = f((state when sender(e)),k) T
es. ( Q(state after e,k))
es. e@destination(l).True
es. (k:. e@destination(l).(n:k. Q((state when e),n)) (n:. Q(state after e,n))) 
x. t(x)
T
t else f fi
}
j < k